es:ES, e:E.
(isrcv(e))
 ((index(e) = 0)
  (e':E.
  (isrcv(e'))
   (sender(e') = sender(e)  E)
   (lnk(e) = lnk(e')  IdLnk)
   e loc e' )) 

latex

Definitions

ES, t  T, x:A. B(x), E, isrcv(e), b, e loc e' , P  Q, lnk(e), IdLnk, s = t, , x:AB(x), sender(e), Type, #$n, index(e), <a, b>, , sends(l;e), (Msg on l), ||as||, {i..j}, {x:A| B(x)} , P  Q, P & Q, P  Q, P  Q, (e <loc e'), loc(e), Id, Void, False, A, x:A  B(x), let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , True, T, destination(l), source(l), left + right, i  j , {T}, Dec(P), a < b, A  B, i  j < k, A c B, x:A. B(x)

Lemmas

es-le-trans2, le wf, decidable int equal, es-locl wf, es-locl-antireflexive, non neg length, es-axioms, lsrc wf, ldst wf, es-loc wf, squash wf, true wf, es-loc-pred, es-index wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-sender wf, IdLnk wf, es-lnk wf, es-le wf, assert wf, es-isrcv wf, es-E wf, event system wf